COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	circum[w87,jmc]		yet another form of circumscription
C00004 ENDMK
C⊗;
circum[w87,jmc]		yet another form of circumscription

Maybe we call it pointwise variable circumscription.

It is defined by minimizing according to the ordering

$$P < P' ≡ (∃x.V(x,x) ∧ P(x) < P'(x)) ∧ ∀y.(P'(y) ≠ P(y) ⊃ ∃x.(
V(x,x) ∧ P(x) < P'(x) ∧ V(x,y))).$$

We conjecture that if  $V - λx.V(x,x)$ is a transitive and irreflexive
ordering, then  $P < P'$ will also be transitive and irreflexive.

What follows is an attempt to write the above to include $c$'s

$$c<c' ≡ (∃i x.V↓{ii}(x,x) ∧ P↓i(x) < P'↓i(x)) ∧ ∀y j.(c'↓j(y) ≠ c↓j(y) ⊃
∃x k.V↓{kk}(x,x) ∧ P↓k(x) < P'↓k(x) ∧ V↓{kj}(x,y)).$$

Vladimir suggests dropping the first clause on the right to get $≤$.
This gives
%
$$c≤c' ≡ ∀y j.(c'↓j(y) ≠ c↓j(y) ⊃ ∃x k.V↓{kk}(x,x) ∧ P↓k(x)<P'↓k(x)∧V↓{kj}(x,y)).$$